(set-logic BV)
(synth-fun f ( (x (BitVec 64)) ) (BitVec 64)
((Start (BitVec 64)
((bvnot Start)
(bvxor Start Start)
(bvand Start Start)
(bvor Start Start)
(bvneg Start)
(bvadd Start Start)
(bvmul Start Start)
(bvudiv Start Start)
(bvurem Start Start)
(bvlshr Start Start)
(bvashr Start Start)
(bvshl Start Start)
(bvsdiv Start Start)
(bvsrem Start Start)
(bvsub Start Start)
x
#x0000000000000000
#x0000000000000001
#x0000000000000002
#x0000000000000003
#x0000000000000004
#x0000000000000005
#x0000000000000006
#x0000000000000007
#x0000000000000008
#x0000000000000009
#x0000000000000009
#x0000000000000009
#x000000000000000A
#x000000000000000B
#x000000000000000C
#x000000000000000D
#x000000000000000E
#x000000000000000F
#x0000000000000010
(ite StartBool Start Start)
))
(StartBool Bool
((= Start Start)
(not StartBool)
(and StartBool StartBool)
(or StartBool StartBool)
))))
(constraint (= (f #xc6d9ca2a1a476208) #x00007fffffffffff))
(constraint (= (f #x21d52b3ce95962b2) #x0000000000000000))
(constraint (= (f #xdb31395a36a8d6b7) #x000024cec6a5c957))
(constraint (= (f #xd80ebc8cd82e75d2) #x000027f1437327d1))
(constraint (= (f #xde521e261c47e2b1) #x000021ade1d9e3b8))
(constraint (= (f #x7221747db4e56e10) #x00000dde8b824b1a))
(constraint (= (f #x3bc37895b63483a8) #x0000000000000000))
(constraint (= (f #x360ce74c7e5e7524) #x0000000000000000))
(constraint (= (f #xc26c5205d9b39599) #x0000000000000001))
(constraint (= (f #x91638300d6ba982a) #x0000000000000000))
(constraint (= (f #x199150417d71684b) #x0000000000000001))
(constraint (= (f #xba54e6be9eb6ceda) #x0000000000000000))
(constraint (= (f #x6ae562cd5325c21c) #x0000151a9d32acda))
(constraint (= (f #xc164330c25e64392) #x00003e9bccf3da19))
(constraint (= (f #x90aa88ca3a4e6ee7) #x00006f557735c5b1))
(constraint (= (f #x1a8107e1711c799a) #x0000000000000000))
(constraint (= (f #x9dc16167a4eebdb3) #x0000623e9e985b11))
(constraint (= (f #x187607d2bd4be1ee) #x00007fffffffffff))
(constraint (= (f #x576ece5132ea46c7) #x0000289131aecd15))
(constraint (= (f #x3085ee2ed0a2e3b3) #x00004f7a11d12f5d))
(constraint (= (f #x0169e79dec57e03b) #x0000000000000001))
(constraint (= (f #x3394ae1ecdd9c6ae) #x0000000000000000))
(constraint (= (f #x3cee8e14e611427e) #x0000000000000000))
(constraint (= (f #x765ec777dbe0b5e1) #x000009a13888241f))
(constraint (= (f #x03cce35e45890bee) #x00007fffffffffff))
(constraint (= (f #x2a8c144d9e8ebb48) #x00007fffffffffff))
(constraint (= (f #xe265a31a05dec442) #x0000000000000000))
(constraint (= (f #x9b7734a85ede3aa5) #x0000000000000001))
(constraint (= (f #xeec23cbc808d54c1) #x0000113dc3437f72))
(constraint (= (f #x8b0ad00e348800d4) #x000074f52ff1cb77))
(constraint (= (f #xed7a00b54584e9cc) #x00007fffffffffff))
(constraint (= (f #x4b697cdd7bc83ee7) #x0000349683228437))
(constraint (= (f #xb5d45a6c5436eeed) #x0000000000000001))
(constraint (= (f #xc06b1bce293e1481) #x0000000000000001))
(constraint (= (f #xd44375526eec6040) #x00007fffffffffff))
(constraint (= (f #xe0e810725d69ed05) #x00001f17ef8da296))
(constraint (= (f #x410bba18c3114adc) #x0000000000000000))
(constraint (= (f #x40cb862ee7c0d35a) #x00003f3479d1183f))
(constraint (= (f #xca355796bc129e14) #x0000000000000000))
(constraint (= (f #x76b0bb3be2ec46e5) #x0000094f44c41d13))
(constraint (= (f #x5a1b3c9a3e54e58a) #x0000000000000000))
(constraint (= (f #xea8863eea8278de4) #x00007fffffffffff))
(constraint (= (f #x27c960b1dbe9ac01) #x000058369f4e2416))
(constraint (= (f #xe3d7192858ea5c66) #x00007fffffffffff))
(constraint (= (f #xd5a3babce956b765) #x0000000000000001))
(constraint (= (f #x7662de82b2226274) #x0000099d217d4ddd))
(constraint (= (f #x8332dc1b1d6e2ab1) #x00007ccd23e4e291))
(constraint (= (f #x21915c6c46788a9d) #x0000000000000001))
(constraint (= (f #x041dc5e9bc7d9eeb) #x0000000000000001))
(constraint (= (f #x170744ede5e9ee09) #x000068f8bb121a16))
(constraint (= (f #xaecc915a17964999) #x0000000000000001))
(constraint (= (f #x61b1d13e00da52d2) #x0000000000000000))
(constraint (= (f #xc62ebd063ece94ea) #x00007fffffffffff))
(constraint (= (f #xb257695e95b03ca8) #x0000000000000000))
(constraint (= (f #xc0aba368608c0754) #x00003f545c979f73))
(constraint (= (f #xb139761e2c5bbcdd) #x0000000000000001))
(constraint (= (f #xe75e617e78e4baa3) #x000018a19e81871b))
(constraint (= (f #x582360ea86ec2741) #x000027dc9f157913))
(constraint (= (f #x5a534269bea58016) #x000025acbd96415a))
(constraint (= (f #x415d99609a837e96) #x00003ea2669f657c))
(constraint (= (f #xe892bc49566abc8e) #x00007fffffffffff))
(constraint (= (f #xd3881d4c19747974) #x0000000000000000))
(constraint (= (f #xee23aa9862813284) #x00007fffffffffff))
(constraint (= (f #x04468a6247ed72b7) #x00007bb9759db812))
(constraint (= (f #xaac70d7968ceed7a) #x00005538f2869731))
(constraint (= (f #x6e4debcc07b76581) #x0000000000000001))
(constraint (= (f #x517330e5e406de57) #x00002e8ccf1a1bf9))
(constraint (= (f #x7e07aeeee0221b1a) #x000001f851111fdd))
(constraint (= (f #xd5e92a54cea4ea03) #x00002a16d5ab315b))
(constraint (= (f #x0b1984ded0a7e49d) #x000074e67b212f58))
(constraint (= (f #x45a5367e4175848d) #x0000000000000001))
(constraint (= (f #x33893e9b5488e516) #x00004c76c164ab77))
(constraint (= (f #x53829635ae207e98) #x00002c7d69ca51df))
(constraint (= (f #x87e97da0aeecc024) #x00007fffffffffff))
(constraint (= (f #x163bda1e27626aa3) #x000069c425e1d89d))
(constraint (= (f #x5c001276335bb915) #x0000000000000001))
(constraint (= (f #xbba6a02781a56406) #x00007fffffffffff))
(constraint (= (f #x5399e467084d0cce) #x00007fffffffffff))
(constraint (= (f #x39e22cb99e7dd51d) #x0000000000000001))
(constraint (= (f #xdcbe481e82aa54be) #x00002341b7e17d55))
(constraint (= (f #xe65a68c15e0bb0d4) #x000019a5973ea1f4))
(constraint (= (f #x4d860ebb7bd8087b) #x0000000000000001))
(constraint (= (f #x2788c104144a9490) #x000058773efbebb5))
(constraint (= (f #x569678b9ae7c7846) #x0000000000000000))
(constraint (= (f #x6cb6eb0daae5c2da) #x0000134914f2551a))
(constraint (= (f #xcb03be52eae65a8e) #x00007fffffffffff))
(constraint (= (f #x71d957db2a917a71) #x0000000000000001))
(constraint (= (f #x02e9966ce1392ecd) #x0000000000000001))
(constraint (= (f #xe3c7233166ee58e9) #x00001c38dcce9911))
(constraint (= (f #xda25105ed463c143) #x000025daefa12b9c))
(constraint (= (f #x2da66edb1e6cac62) #x00007fffffffffff))
(constraint (= (f #x92a6eaa9c1de9bba) #x0000000000000000))
(constraint (= (f #xce4059e0ea4555cd) #x000031bfa61f15ba))
(constraint (= (f #x06d693e06098591a) #x0000000000000000))
(constraint (= (f #xd8e4bb46334828d4) #x0000271b44b9ccb7))
(constraint (= (f #x970b0be9814565ec) #x00007fffffffffff))
(constraint (= (f #x25ee818ac08a4e18) #x00005a117e753f75))
(constraint (= (f #xd06e7e253763424c) #x00007fffffffffff))
(constraint (= (f #xee5d5464dad010a2) #x0000000000000000))
(constraint (= (f #x287e4ee4518e0c4e) #x00007fffffffffff))
(check-synth)
